Formal systems {axiomatic theory} can have primitives, definitions, axioms, and postulates in theory language {object language}.
primitive terms
Object language has undefined primitive symbols or objects.
definitions
Combining primitive terms defines further symbols or objects.
axioms
Combining primitives and definitions can make assumptions. Axioms assume identity element existence, inverse element existence, commutation law, association law, and distribution law. Axioms are independent of other axioms.
postulates
Object languages have valid statement structures and have logical rules for transforming statement structures. For example, variables can take values.
proofs
Starting from primitive terms, definitions, axioms, and postulates, logic can prove theorem or formula statements, by deduction and formal proofs.
examples
First-order predicate calculus {standard formalization} {first-order theory} is an example.
equivalences
The same axiomatic theory can use different symbols and relations {formulation} {model, axiomatic theory}. Axiomatic-theory primitive terms and relations can have different meanings {interpretation, axiomatic theory} {representation, axiomatic theory}.
Axiomatic theories using different symbols and relations can be formally the same {isomorphism, axiomatic theory}. Axiomatic theories can always have isomorphic forms {representation theorem}. Categorical theory shows how to prove that two axiomatic theories are isomorphic.
In axiomatic theories, contradiction means that statement and its inverse are true. If no theorem can contradict any axiom or theorem {consistency, mathematics}, statements and their inverses cannot both be true. Inconsistent theories have proofs that start with axiom or theorem and lead to inverse and so contradiction.
Formal-system symbols, words, axioms, coding, and rules have intended representation {standard interpretation}. If formal system is consistent, nonstandard interpretations exist that make statements that were false in standard interpretations true in nonstandard interpretations.
For axiomatic theories, does algorithm exist that can determine if formula is true or false {decision problem}? Do algorithms exist that can determine if formulas with no variables are true or false? Does showing that formula is true or false require formal proof?
In axiomatic theories that contain number theory, it is impossible to decide whether formula is true by any method except formal proof {Church's thesis, truth} {Church thesis, truth}.
Logical-principle and simple formal-system theory {metamathematics} {proof theory, mathematics} can have no infinities, use minimum English, use existence theorems to show how to construct new objects, not use proof by contradiction, not use Zorn's lemma, and not use axiom of choice [Hilbert, 1899] [Kleene, 1952] [Tarski, 1983].
Axiomatic-theory object languages can use higher-level natural-language terms {metalanguage} {syntax language}. Higher-level languages express theorems {metatheorem} about proofs, formal theories, languages, and logic [Hilbert, 1899] [Kleene, 1952] [Tarski, 1983]. Metamathematics is a metalanguage.
Mathematics can use only ideas of relation and class {logic of relations} {pure mathematics}.
Axiomatic theories can prove all theorems from terms and axioms {completeness, mathematics}. For example, propositional calculus and predicate calculus are complete. Incomplete theories cannot prove at least one true statement from terms and axioms.
d-completeness
Complete theories can not allow new axioms {d-completeness}, because new axioms cause contradiction. For example, propositional calculus is d-complete. Predicate calculus is not d-complete, because it can add new axioms without contradicting any axiom or theorem and then use that axiom to prove more theorems.
Formal mathematical system, such as arithmetic, algebra, geometry, or set theory, has true propositions that people cannot prove true or false using theory definitions, axioms, rules, and theorems {completeness theorem} {Gödel completeness theorem} {Gödel's theorem} {incompleteness theorem}. Formal mathematical system that includes all true mathematics theorems cannot exist.
formal system
Formal mathematical systems have finite numbers of word and symbol definitions, assumed-true axioms, and rules for combining words, symbols, and statements. Propositions combine words, symbols, and axioms. Typically, formal systems can form an infinite number of propositions.
For example, arithmetic is a formal mathematical system. It defines real numbers; sign symbols, such as plus and minus; operation symbols, such as addition and multiplication; grouping symbols, such as parentheses, brackets, commas, and spaces; variable symbols, such as x and y; proposition and axiom symbols, such as A and B; quantifier symbols, such as existential quantifier and universal quantifier; and logic symbols, such as AND, OR, NOT, IMPLIES, and IF. Arithmetic has axioms, such as commutation and association, about addition and multiplication operations. Arithmetic has axioms that are logic truths, such as "NOT of NOT of statement is statement", and "NOT of function existential quantifier is equivalent to universal quantifier for function NOT". Arithmetic has rules to derive propositions from previous propositions, for example, specifying variable value. Important rule is "If implication premise is true and implication is true, conclusion is true." Arithmetic can use word and symbol definitions, axioms, and rules to calculate and represent variables and functions.
proof
Formal-mathematical-system purpose is to prove propositions true or false. Proofs are proposition series that use axioms, rules, and theorems to go from premise to conclusion. Valid formal mathematical systems prove true theorems and disprove false statements. Later proofs can use proved theorems.
natural number
Natural numbers are finite digit sequences, with no signs or symbols. Natural numbers can have binary coding.
code array
Because formal systems have finite parts and countable propositions, unique natural numbers can represent words, symbols, axioms, propositions, theorems, and rules. Proposition series can be unique natural-number series, and coded proofs are countable unique natural-number series. Listing all natural numbers represents the formal mathematical system. Number of binary digits needed to express all mathematical-system propositions and proofs is the same as number of propositions and proofs. Therefore, list length is the same as width. See Figure 1.
constructing new natural number
Starting from unique natural-number list, one can construct a new natural number that is not in original system by the following method. Start with diagonal {diagonal slash} of the square list. See Figure 2.
Change marks at intersections of first row and column, second row and column, and so on. See Figure 3. New digit sequence has same length as the others and is unique natural number. It is not the same as any row or column sequence. It differs from first row and column at first number, differs from second row and column at second number, and so on.
completeness
The unique natural number represents a statement that was not in original system. However, original list contained all system propositions. Therefore, no formal mathematical system can be complete. One can always derive new statements.
consistency
Original list contained all proven system propositions, so new statement has no proof yet. New proposition is derivable from system but is neither true nor false yet. System plus new statement is indeterminate and inconsistent.
incompleteness or inconsistency
If system lacks the proposition proof, proposition does not have correct form. However, proposition came directly from original propositions and so must have correct form. Therefore, statement is part of formal system but is indeterminate in trueness or falseness. Such formal systems are not consistent.
If system has the proposition proof, proposition is in current system but was not in original system. Such formal systems were incomplete.
If a formal system has only true propositions, and if the system does not prove the newly derived proposition, NOT of new proposition is false, because system already has all true-proposition proofs. New proposition is true, but its proof is not in system. Such systems are inconsistent.
If a formal system has only true propositions, and if the system does prove the newly derived proposition, new proposition is true, because all proven statements are true. However, all true propositions were already in system. Such systems were incomplete.
Formal systems must be either incomplete or inconsistent.
question
Number of binary digits needed to express all mathematical-system propositions and proofs is the same as number of propositions and proofs, so another binary digit must be added to all original propositions and to new proposition. To make a valid formal system, adding a proposition must change the original propositions. Note: Added binary digit can be the same as or different from added binary digit in original statements. Perhaps, the new system can be complete and consistent.
Perhaps, formal system can have proofs for all true statements {omega consistency, completeness}. However, the incompleteness theorem demonstrates that consistent formal system has at least one true statement that has no proof and so is incomplete, as shown by Gödel. Incompleteness theorem shows that the proposition that formal system is omega consistent is not provable by the formal system. For example, logic and number theory have no proof that they are consistent using formal number theory. Therefore, information derivable from formal systems has limits. No axiom set is sufficient to prove all arithmetic or mathematics, by Gödel's proof.
If "one" has a property, and number successors have the property, all numbers have the property {mathematical induction postulate} {induction postulate}. It is a Dedekind-Peano postulate.
Positive-integer axiomatic theory has postulates {Peano's postulates} {Peano postulates} {Dedekind-Peano postulates}. "One" is a number. The number "one" is not any number's successor. A number successor is a number. No two numbers have same successor. If "one" has property and if number successor has property, all numbers have property {induction postulate, Peano}.
Geometry is an axiomatic system {geometry theory}.
primitives
Geometry can use two undefined ideas: point and order.
symbols
Geometry can use three symbols: point or line, segment, and motion or congruence. Points can be ordered-pairs. Line can be a ratio. Congruence can be translation, rotation, and reflection.
axioms
Points can form a set. At least one point exists. If there is a point, then there is another point. Given two points, there are lines. Given a line, there is another line. Given two lines, there is a space.
postulates
Axiomatized geometry has five postulates, similar to Euclid's five postulates. Lines can have no multiple points {Jordan curve, geometry}. Figures can have infinite perimeters.
In three-dimensional space, continuity axiom is true, but planes and surfaces do not need this axiom.
Dimension number is not necessarily coordinate number or point multiplicity.
theory
Geometry uses point, line, plane, how point "lies on" line, how point "lies on" plane, how point pairs are congruent, how angles are congruent, and/or how points order on lines {betweenness, geometry}.
consistency
Geometry is consistent if arithmetic is consistent.
Counting numbers, and all numbers, can form an axiomatic theory {natural number theory}.
axioms
Start with null set and with two axioms. Numbers correspond to two sets of previously constructed numbers, with no member of left set greater than or equal to members of right set. Number is less than or equal to another number, if and only if no member of first-number left set is greater than or equal to second number and no member of second-number right set is less than or equal to first number.
axioms: procedure
First, make null set both right and left set, to obtain number zero. Then make right set null and left set contain number zero to obtain number one. Continue to build all counting numbers. All other numbers can derive from counting numbers.
equivalence
Equivalence or one-to-one correspondence can construct counting numbers. Start with null set. Define zero as cardinal number of elements in null set and equivalent sets. Define one as number of elements in set that contains only zero as element. Define two as number of elements in set that contains only elements zero and one. Define N as number of elements in set that contains only elements zero through N.
numbers in general
Axiomatizing natural numbers allows axiomatizing all number types. The number "one" belongs to a set. Set members have one and only one successor. If two successors are equal, then members are equal. The number "one" is not any number's successor. If subset contains "one" and another number, then number successor is in subset and subset is same as whole set.
integers
Positive integers can be an axiomatic system. Undefined terms are "one", "number", and "successor of". Dedekind-Peano postulates can construct the positive integers.
Geometries {non-Archimedian geometry} that violate Archimedes axiom can be axiomatic systems.
Outline of Knowledge Database Home Page
Description of Outline of Knowledge Database
Date Modified: 2022.0225